00100	PRE_OP:J,C,M,N;
00200	PRE_PRED:P,R,Q;
00300	VAR:X1,X2,X3,X4;
01700	∀(X1,X2,X3,X4) ((((P(X1,X2)∨P(X2,X1))∧(P(X3,X4)∨P(X4,X3)))∧
01800	  ((P(X1,X2)∧P(X3,X4))→Q(J(M(N,X3),M(C(N),X2)),J(M(N,X1),M(C(N),X4))))
02100	∧ ((P(X2,X1)∧P(X3,X4))→Q(J(M(N,X3),M(C(N),X1)),J(M(N,X2),M(C(N),X4)))))
02200	→R(X1,X2,X3,X4));;
02300	∀(X1,X2,X3,X4) (R(X1,X2,X3,X4)∨R(X3,X4,X1,X2));;